feat: Lean 4 analyzer, with header-scanner structure and exact-name resolution - #158

Summary

Adds a Lean 4 analyzer, with the two-layer design agreed in #154.

Stacked on #156. This PR targets main, because GitHub cannot use a
fork branch as the base. Its first two commits are #156. Review only the
last two commits, feat: Lean 4 analyzer, ... and a
format fix of its test. I will rebase this PR when #156
is merged.

Design

1. Structure, from a header scanner. Comments, strings and char literals
   are masked with spaces of the same UTF-8 length, so lines and byte offsets
   do not move. The scanner then reads the Lean commands line by line:
   • declarations: def, theorem/lemma, abbrev, instance,
     structure, class, class inductive, inductive, axiom and
     opaque, with attributes and modifiers
   • the namespace/section/mutual/end stack, and open, also
     open X in
   • import, spans, and /-- -/ docstrings
     It does not use the parse tree, so an ERROR region does not hide a
     declaration.
2. References, from tree-sitter. The analyzer takes each identifier
   node in the lines of a declaration, also the nodes inside ERROR nodes.
   Text that an ERROR node does not cover with child nodes is tokenized
   from the masked source. Local names are removed: binders, let, have,
   fun, intro/obtain, match patterns, and a dotted name whose first
   part is local (p.x).

Resolution is in CallGraphAnalyzer, as for Go and Dart:

• A reference resolves only to an exact fully qualified name. The candidates
  are, in Lean's order:
  1. the namespaces of the declaration, innermost first
  2. the root namespace
  3. the open namespaces
• Only the caller's file and the files that it imports (transitively) are
  visible. An import maps to a file by its path suffix (Geo.Point to
  src/Geo/Point.lean), because the Lake source folder is not known. A
  private name is visible only in its own file.
• No match, or more than one, drops the reference. A lean branch in
  _resolve_callee and _has_authoritative_resolution stops the name-only
  fallback.
• Constructor and field names (Point.mk, Point.x, Shape.dot) link to
  their structure or inductive. When a whole dotted name matches nothing,
  its longest prefix that matches is the constant, and the rest are
  projections (origin.x links to origin).

Other parts:

• Component types: structure is struct, class is interface,
  inductive is class, and the rest are function. node_type keeps the
  keyword (lemma becomes theorem).
• An anonymous instance is named instance_L<line>.
• .lake/ and lake-packages/ are skipped. lakefile.lean and
  lakefile.toml are build artifacts, and lake-manifest.json and
  lean-toolchain are manifests.
• Lean is registered in the file discovery, the CLI validators, the MCP
  tools and the graph viewer (lang-lean). The Docker image downloads the
  lean grammar. The grammar test of deps: move tree-sitter-language-pack to 1.x, with a clear error when a grammar cannot be downloaded #156 checks the Dockerfile list.

Known limits

These are the limits from #154, plus three that I found during the work:

• Generalized field notation on a value (v.norm for Vec.norm) needs type
  information, so it does not resolve.
• References made through user notation/macro are lost.
• The scanner assumes that each command starts a line. A declaration ends at
  the next command at the same or a smaller indentation.
• Local names are removed by name for the whole declaration. So a global
  that has the same simple name as a local of that declaration is not linked.
• Lean's overload resolution among open namespaces uses types. Here, two
  matches in the open namespaces drop the reference.

Measurement

I ran it on a private corpus of 1,066 Lean 4 files (programs and proofs, not
Mathlib), and I checked 300 sampled files:

• The regex reads comments and syntax quotations as code. The misses that I
  checked were all in those regions, not real declarations.
• The corpus includes generated files of more than 13,000 lines. The time
  is small next to the LLM phase of a run.

Tests

• tests/test_lean_analyzer.py (new, 21 tests, synthetic Lean only):
  • declarations, namespaces and component types
  • spans, docstrings and attributes
  • skipped Lake folders
  • same-file, open X in, imported and alias edges
  • ERROR regions
  • locals, externals and recursion
  • private and not-imported names
  • ambiguous names, _root_ and mutual
  • masking, including interpolated strings and primes
• tests/test_artifact_analyzer.py has rows for the Lake files.
• The full suite gives 699 passed and 1 failed.
  test_doc_write_guard.py::test_warning_reports_rejected_tool_calls also
  fails on main, as noted in deps: move tree-sitter-language-pack to 1.x, with a clear error when a grammar cannot be downloaded #156.
• ruff check and ruff format --check pass.

Note: tests/test_lean_analyzer.py is added with git add -f, because of
tests/* in .gitignore.

Closes #154

🤖 Generated with Claude Code